Nuprl Lemma : eqmod_functionality_wrt_eqmod 2,24

mm'aa'bb':.
m = m'  (a = a' mod m (b = b' mod m ((a = b mod m (a' = b' mod m')) 
latex


DefinitionsP  Q, P & Q, P  Q, P  Q, a = b mod m, x:AB(x), Prop, t  T
Lemmaseqmod transitivity, eqmod inversion, eqmod wf

origin